'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(x)
, top(active(c())) -> top(mark(c()))
, top(mark(x)) -> top(check(x))
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, start(ok(x)) -> found(x)
, f(found(x)) -> found(f(x))
, top(found(x)) -> top(active(x))
, active(f(x)) -> f(active(x))
, f(mark(x)) -> mark(f(x))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(f(x)) -> c_0()
, top^#(active(c())) -> c_1(top^#(mark(c())))
, top^#(mark(x)) -> c_2(top^#(check(x)))
, check^#(f(x)) -> c_3(f^#(check(x)))
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))
, match^#(X(), x) -> c_6(proper^#(x))
, proper^#(c()) -> c_7()
, proper^#(f(x)) -> c_8(f^#(proper(x)))
, f^#(ok(x)) -> c_9(f^#(x))
, start^#(ok(x)) -> c_10()
, f^#(found(x)) -> c_11(f^#(x))
, top^#(found(x)) -> c_12(top^#(active(x)))
, active^#(f(x)) -> c_13(f^#(active(x)))
, f^#(mark(x)) -> c_14(f^#(x))}
The usable rules are:
{ active(f(x)) -> mark(x)
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, active(f(x)) -> f(active(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)}
The estimated dependency graph contains the following edges:
{top^#(active(c())) -> c_1(top^#(mark(c())))}
==> {top^#(mark(x)) -> c_2(top^#(check(x)))}
{top^#(mark(x)) -> c_2(top^#(check(x)))}
==> {top^#(found(x)) -> c_12(top^#(active(x)))}
{top^#(mark(x)) -> c_2(top^#(check(x)))}
==> {top^#(mark(x)) -> c_2(top^#(check(x)))}
{check^#(f(x)) -> c_3(f^#(check(x)))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{check^#(f(x)) -> c_3(f^#(check(x)))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{check^#(f(x)) -> c_3(f^#(check(x)))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
{check^#(x) -> c_4(start^#(match(f(X()), x)))}
==> {start^#(ok(x)) -> c_10()}
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
{match^#(X(), x) -> c_6(proper^#(x))}
==> {proper^#(f(x)) -> c_8(f^#(proper(x)))}
{match^#(X(), x) -> c_6(proper^#(x))}
==> {proper^#(c()) -> c_7()}
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
{f^#(ok(x)) -> c_9(f^#(x))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{f^#(ok(x)) -> c_9(f^#(x))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{f^#(ok(x)) -> c_9(f^#(x))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
{f^#(found(x)) -> c_11(f^#(x))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{f^#(found(x)) -> c_11(f^#(x))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{f^#(found(x)) -> c_11(f^#(x))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
{top^#(found(x)) -> c_12(top^#(active(x)))}
==> {top^#(found(x)) -> c_12(top^#(active(x)))}
{top^#(found(x)) -> c_12(top^#(active(x)))}
==> {top^#(mark(x)) -> c_2(top^#(check(x)))}
{top^#(found(x)) -> c_12(top^#(active(x)))}
==> {top^#(active(c())) -> c_1(top^#(mark(c())))}
{active^#(f(x)) -> c_13(f^#(active(x)))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{active^#(f(x)) -> c_13(f^#(active(x)))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{active^#(f(x)) -> c_13(f^#(active(x)))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
{f^#(mark(x)) -> c_14(f^#(x))}
==> {f^#(mark(x)) -> c_14(f^#(x))}
{f^#(mark(x)) -> c_14(f^#(x))}
==> {f^#(found(x)) -> c_11(f^#(x))}
{f^#(mark(x)) -> c_14(f^#(x))}
==> {f^#(ok(x)) -> c_9(f^#(x))}
We consider the following path(s):
1) { top^#(active(c())) -> c_1(top^#(mark(c())))
, top^#(found(x)) -> c_12(top^#(active(x)))
, top^#(mark(x)) -> c_2(top^#(check(x)))}
The usable rules for this path are the following:
{ active(f(x)) -> mark(x)
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, active(f(x)) -> f(active(x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(x)
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, active(f(x)) -> f(active(x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, top^#(active(c())) -> c_1(top^#(mark(c())))
, top^#(found(x)) -> c_12(top^#(active(x)))
, top^#(mark(x)) -> c_2(top^#(check(x)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [4]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [1] x1 + [4]
c_1(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))}
and weakly orienting the rules
{ active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [6]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [4]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [4]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [10]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [1] x1 + [2]
c_1(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [4]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{ check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))
, active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [9]
start(x1) = [1] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [4]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [4]
found(x1) = [1] x1 + [14]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(X(), x) -> proper(x)}
and weakly orienting the rules
{ match(f(x), f(y)) -> f(match(x, y))
, check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))
, active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(X(), x) -> proper(x)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [1]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [8]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [1] x1 + [3]
c_1(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [1]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{start(ok(x)) -> found(x)}
and weakly orienting the rules
{ match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))
, active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{start(ok(x)) -> found(x)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [2]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
c() = [8]
check(x1) = [1] x1 + [15]
start(x1) = [1] x1 + [7]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [8]
proper(x1) = [1] x1 + [8]
ok(x1) = [1] x1 + [3]
found(x1) = [1] x1 + [9]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [1] x1 + [11]
c_1(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [9]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [2]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ check(f(x)) -> f(check(x))
, active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))
, top^#(mark(x)) -> c_2(top^#(check(x)))}
Weak Rules:
{ start(ok(x)) -> found(x)
, match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))
, active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ check(f(x)) -> f(check(x))
, active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))
, top^#(mark(x)) -> c_2(top^#(check(x)))}
Weak Rules:
{ start(ok(x)) -> found(x)
, match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, check(x) -> start(match(f(X()), x))
, top^#(active(c())) -> c_1(top^#(mark(c())))
, active(f(x)) -> mark(x)
, proper(c()) -> ok(c())
, top^#(found(x)) -> c_12(top^#(active(x)))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ active_0(2) -> 4
, active_1(2) -> 14
, f_1(9) -> 8
, f_2(19) -> 18
, mark_0(2) -> 2
, mark_1(12) -> 11
, c_0() -> 2
, c_1() -> 12
, check_1(2) -> 6
, check_2(12) -> 16
, start_1(7) -> 6
, start_2(17) -> 6
, start_2(20) -> 16
, match_1(8, 2) -> 7
, match_2(18, 2) -> 17
, match_2(18, 12) -> 20
, X_0() -> 2
, X_1() -> 9
, X_2() -> 19
, ok_0(2) -> 2
, found_0(2) -> 2
, top^#_0(2) -> 1
, top^#_0(4) -> 3
, top^#_1(6) -> 5
, top^#_1(11) -> 10
, top^#_1(14) -> 13
, top^#_2(16) -> 15
, c_1_1(10) -> 3
, c_1_1(10) -> 13
, c_2_1(5) -> 1
, c_2_2(15) -> 10
, c_12_0(3) -> 1
, c_12_1(13) -> 1}
2) { check^#(f(x)) -> c_3(f^#(check(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
The usable rules for this path are the following:
{ check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, check^#(f(x)) -> c_3(f^#(check(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{check^#(f(x)) -> c_3(f^#(check(x)))}
and weakly orienting the rules
{ start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{check^#(f(x)) -> c_3(f^#(check(x)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [2]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [2]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [5]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ match(X(), x) -> proper(x)
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
and weakly orienting the rules
{ check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ match(X(), x) -> proper(x)
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [12]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [9]
match(x1, x2) = [1] x1 + [1] x2 + [8]
X() = [8]
proper(x1) = [1] x1 + [5]
ok(x1) = [1] x1 + [4]
found(x1) = [1] x1 + [12]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [8]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{ match(X(), x) -> proper(x)
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [10]
mark(x1) = [1] x1 + [7]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [3]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [14]
X() = [2]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [7]
c_3(x1) = [1] x1 + [5]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [3]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{check(x) -> start(match(f(X()), x))}
and weakly orienting the rules
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{check(x) -> start(match(f(X()), x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
c() = [2]
check(x1) = [1] x1 + [2]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [1]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [3]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [8]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ check(f(x)) -> f(check(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ check(f(x)) -> f(check(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, check^#_0(3) -> 18
, check^#_0(5) -> 18
, check^#_0(9) -> 18
, check^#_0(11) -> 18
, check^#_0(12) -> 18
, f^#_0(3) -> 20
, f^#_0(5) -> 20
, f^#_0(9) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20
, c_9_0(20) -> 20
, c_11_0(20) -> 20
, c_14_0(20) -> 20}
3) { match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
The usable rules for this path are the following:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [9]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(x)) -> c_9(f^#(x))}
and weakly orienting the rules
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(x)) -> c_9(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [1] x1 + [7]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(x)) -> c_14(f^#(x))}
and weakly orienting the rules
{ f^#(ok(x)) -> c_9(f^#(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(x)) -> c_14(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))}
and weakly orienting the rules
{ f^#(mark(x)) -> c_14(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [3]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [6]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [8]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(X(), x) -> proper(x)}
and weakly orienting the rules
{ proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(X(), x) -> proper(x)}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [11]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [8]
X() = [8]
proper(x1) = [1] x1 + [12]
ok(x1) = [1] x1 + [2]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [5]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [13]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{ match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [6]
mark(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [8]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [13]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, f^#_0(3) -> 20
, f^#_0(5) -> 20
, f^#_0(9) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20
, match^#_0(3, 3) -> 23
, match^#_0(3, 5) -> 23
, match^#_0(3, 9) -> 23
, match^#_0(3, 11) -> 23
, match^#_0(3, 12) -> 23
, match^#_0(5, 3) -> 23
, match^#_0(5, 5) -> 23
, match^#_0(5, 9) -> 23
, match^#_0(5, 11) -> 23
, match^#_0(5, 12) -> 23
, match^#_0(9, 3) -> 23
, match^#_0(9, 5) -> 23
, match^#_0(9, 9) -> 23
, match^#_0(9, 11) -> 23
, match^#_0(9, 12) -> 23
, match^#_0(11, 3) -> 23
, match^#_0(11, 5) -> 23
, match^#_0(11, 9) -> 23
, match^#_0(11, 11) -> 23
, match^#_0(11, 12) -> 23
, match^#_0(12, 3) -> 23
, match^#_0(12, 5) -> 23
, match^#_0(12, 9) -> 23
, match^#_0(12, 11) -> 23
, match^#_0(12, 12) -> 23
, c_9_0(20) -> 20
, c_11_0(20) -> 20
, c_14_0(20) -> 20}
4) { match^#(X(), x) -> c_6(proper^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
The usable rules for this path are the following:
{ proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))
, match^#(X(), x) -> c_6(proper^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(x)) -> c_9(f^#(x))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(x)) -> c_9(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match^#(X(), x) -> c_6(proper^#(x))}
and weakly orienting the rules
{f^#(ok(x)) -> c_9(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match^#(X(), x) -> c_6(proper^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(x)) -> c_14(f^#(x))}
and weakly orienting the rules
{ match^#(X(), x) -> c_6(proper^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(x)) -> c_14(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [8]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [0]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10() = [0]
c_11(x1) = [1] x1 + [10]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
and weakly orienting the rules
{ f^#(mark(x)) -> c_14(f^#(x))
, match^#(X(), x) -> c_6(proper^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(found(x)) -> c_11(f^#(x))}
and weakly orienting the rules
{ proper^#(f(x)) -> c_8(f^#(proper(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, match^#(X(), x) -> c_6(proper^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(found(x)) -> c_11(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [4]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7() = [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{ f^#(found(x)) -> c_11(f^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, match^#(X(), x) -> c_6(proper^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [1]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [8]
proper(x1) = [1] x1 + [8]
ok(x1) = [1] x1 + [4]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [12]
c_7() = [0]
c_8(x1) = [1] x1 + [3]
c_9(x1) = [1] x1 + [4]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, match^#(X(), x) -> c_6(proper^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ proper(c()) -> ok(c())
, f^#(found(x)) -> c_11(f^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, match^#(X(), x) -> c_6(proper^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, f^#_0(3) -> 20
, f^#_0(5) -> 20
, f^#_0(9) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20
, match^#_0(3, 3) -> 23
, match^#_0(3, 5) -> 23
, match^#_0(3, 9) -> 23
, match^#_0(3, 11) -> 23
, match^#_0(3, 12) -> 23
, match^#_0(5, 3) -> 23
, match^#_0(5, 5) -> 23
, match^#_0(5, 9) -> 23
, match^#_0(5, 11) -> 23
, match^#_0(5, 12) -> 23
, match^#_0(9, 3) -> 23
, match^#_0(9, 5) -> 23
, match^#_0(9, 9) -> 23
, match^#_0(9, 11) -> 23
, match^#_0(9, 12) -> 23
, match^#_0(11, 3) -> 23
, match^#_0(11, 5) -> 23
, match^#_0(11, 9) -> 23
, match^#_0(11, 11) -> 23
, match^#_0(11, 12) -> 23
, match^#_0(12, 3) -> 23
, match^#_0(12, 5) -> 23
, match^#_0(12, 9) -> 23
, match^#_0(12, 11) -> 23
, match^#_0(12, 12) -> 23
, c_6_0(26) -> 23
, proper^#_0(3) -> 26
, proper^#_0(5) -> 26
, proper^#_0(9) -> 26
, proper^#_0(11) -> 26
, proper^#_0(12) -> 26
, c_9_0(20) -> 20
, c_11_0(20) -> 20
, c_14_0(20) -> 20}
5) { active^#(f(x)) -> c_13(f^#(active(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
The usable rules for this path are the following:
{ active(f(x)) -> mark(x)
, active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(x)
, active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, active^#(f(x)) -> c_13(f^#(active(x)))
, f^#(mark(x)) -> c_14(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(ok(x)) -> c_9(f^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active(f(x)) -> mark(x)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(x)) -> mark(x)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [1]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(f(x)) -> c_13(f^#(active(x)))}
and weakly orienting the rules
{active(f(x)) -> mark(x)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(x)) -> c_13(f^#(active(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [8]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [3]
c_14(x1) = [1] x1 + [4]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(x)) -> c_14(f^#(x))}
and weakly orienting the rules
{ active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(x)) -> c_14(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(found(x)) -> c_11(f^#(x))}
and weakly orienting the rules
{ f^#(mark(x)) -> c_14(f^#(x))
, active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(found(x)) -> c_11(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [4]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
found(x1) = [1] x1 + [7]
active^#(x1) = [1] x1 + [15]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [11]
c_10() = [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(x)) -> c_9(f^#(x))}
and weakly orienting the rules
{ f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(x)) -> c_9(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [2]
f(x1) = [1] x1 + [2]
mark(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [10]
found(x1) = [1] x1 + [2]
active^#(x1) = [1] x1 + [13]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [6]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [5]
c_10() = [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [1] x1 + [2]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ f^#(ok(x)) -> c_9(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ f^#(ok(x)) -> c_9(f^#(x))
, f^#(found(x)) -> c_11(f^#(x))
, f^#(mark(x)) -> c_14(f^#(x))
, active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, ok_0(3) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, active^#_0(3) -> 13
, active^#_0(11) -> 13
, active^#_0(12) -> 13
, f^#_0(3) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20
, c_9_0(20) -> 20
, c_11_0(20) -> 20
, c_14_0(20) -> 20}
6) {check^#(f(x)) -> c_3(f^#(check(x)))}
The usable rules for this path are the following:
{ check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, check^#(f(x)) -> c_3(f^#(check(x)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{check^#(f(x)) -> c_3(f^#(check(x)))}
and weakly orienting the rules
{ start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{check^#(f(x)) -> c_3(f^#(check(x)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [1]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{ check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
c() = [2]
check(x1) = [1] x1 + [9]
start(x1) = [1] x1 + [1]
match(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [1]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [13]
c_3(x1) = [1] x1 + [8]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(X(), x) -> proper(x)}
and weakly orienting the rules
{ check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(X(), x) -> proper(x)}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [1] x1 + [2]
start(x1) = [1] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ check(f(x)) -> f(check(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ match(X(), x) -> proper(x)
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ check(f(x)) -> f(check(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ match(X(), x) -> proper(x)
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, check^#(f(x)) -> c_3(f^#(check(x)))
, start(ok(x)) -> found(x)
, proper(c()) -> ok(c())}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, check^#_0(3) -> 18
, check^#_0(5) -> 18
, check^#_0(9) -> 18
, check^#_0(11) -> 18
, check^#_0(12) -> 18
, f^#_0(3) -> 20
, f^#_0(5) -> 20
, f^#_0(9) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20}
7) { check^#(x) -> c_4(start^#(match(f(X()), x)))
, start^#(ok(x)) -> c_10()}
The usable rules for this path are the following:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, start^#(ok(x)) -> c_10()}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{check^#(x) -> c_4(start^#(match(f(X()), x)))}
and weakly orienting the rules
{proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{check^#(x) -> c_4(start^#(match(f(X()), x)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
c() = [2]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [8]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{start^#(ok(x)) -> c_10()}
and weakly orienting the rules
{ check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{start^#(ok(x)) -> c_10()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [12]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [7]
start^#(x1) = [1] x1 + [1]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(X(), x) -> proper(x)}
and weakly orienting the rules
{ start^#(ok(x)) -> c_10()
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(X(), x) -> proper(x)}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [13]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [8]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
start^#(x1) = [1] x1 + [1]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{ match(X(), x) -> proper(x)
, start^#(ok(x)) -> c_10()
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
c() = [4]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [5]
proper(x1) = [1] x1 + [4]
ok(x1) = [1] x1 + [4]
found(x1) = [1] x1 + [4]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [13]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [3]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, start^#(ok(x)) -> c_10()
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, start^#(ok(x)) -> c_10()
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ f_0(9) -> 25
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, match_0(25, 3) -> 24
, match_0(25, 5) -> 24
, match_0(25, 9) -> 24
, match_0(25, 11) -> 24
, match_0(25, 12) -> 24
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, check^#_0(3) -> 18
, check^#_0(5) -> 18
, check^#_0(9) -> 18
, check^#_0(11) -> 18
, check^#_0(12) -> 18
, c_4_0(23) -> 18
, start^#_0(3) -> 22
, start^#_0(5) -> 22
, start^#_0(9) -> 22
, start^#_0(11) -> 22
, start^#_0(12) -> 22
, start^#_0(24) -> 23
, c_10_0() -> 22}
8) {match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
The usable rules for this path are the following:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [4]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [6]
mark(x1) = [1] x1 + [10]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(X(), x) -> proper(x)}
and weakly orienting the rules
{ match(f(x), f(y)) -> f(match(x, y))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(X(), x) -> proper(x)}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [10]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [9]
X() = [2]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [13]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [4]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [13]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{ match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [7]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [2]
X() = [14]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [8]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [5]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [15]
c_5(x1) = [1] x1 + [4]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ proper(c()) -> ok(c())
, match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ proper(c()) -> ok(c())
, match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, match^#(f(x), f(y)) -> c_5(f^#(match(x, y)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, c_0() -> 2
, X_0() -> 2
, ok_0(2) -> 2
, found_0(2) -> 2
, f^#_0(2) -> 1
, match^#_0(2, 2) -> 1}
9) {check^#(x) -> c_4(start^#(match(f(X()), x)))}
The usable rules for this path are the following:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, check^#(x) -> c_4(start^#(match(f(X()), x)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{check^#(x) -> c_4(start^#(match(f(X()), x)))}
and weakly orienting the rules
{proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{check^#(x) -> c_4(start^#(match(f(X()), x)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [8]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(f(x), f(y)) -> f(match(x, y))}
and weakly orienting the rules
{ check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(f(x), f(y)) -> f(match(x, y))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [8]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [12]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match(X(), x) -> proper(x)}
and weakly orienting the rules
{ match(f(x), f(y)) -> f(match(x, y))
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match(X(), x) -> proper(x)}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [1]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [1] x1 + [8]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
start^#(x1) = [1] x1 + [1]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, proper(f(x)) -> f(proper(x))}
Weak Rules:
{ match(X(), x) -> proper(x)
, match(f(x), f(y)) -> f(match(x, y))
, check^#(x) -> c_4(start^#(match(f(X()), x)))
, proper(c()) -> ok(c())}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ f_0(9) -> 25
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, match_0(25, 3) -> 24
, match_0(25, 5) -> 24
, match_0(25, 9) -> 24
, match_0(25, 11) -> 24
, match_0(25, 12) -> 24
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, check^#_0(3) -> 18
, check^#_0(5) -> 18
, check^#_0(9) -> 18
, check^#_0(11) -> 18
, check^#_0(12) -> 18
, c_4_0(23) -> 18
, start^#_0(3) -> 22
, start^#_0(5) -> 22
, start^#_0(9) -> 22
, start^#_0(11) -> 22
, start^#_0(12) -> 22
, start^#_0(24) -> 23}
10)
{ match^#(X(), x) -> c_6(proper^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))}
The usable rules for this path are the following:
{ proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, match^#(X(), x) -> c_6(proper^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [8]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{match^#(X(), x) -> c_6(proper^#(x))}
and weakly orienting the rules
{proper^#(f(x)) -> c_8(f^#(proper(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match^#(X(), x) -> c_6(proper^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
found(x1) = [1] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [3]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{ match^#(X(), x) -> c_6(proper^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [15]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [6]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [8]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [7]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [11]
c_7() = [0]
c_8(x1) = [1] x1 + [8]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ proper(c()) -> ok(c())
, match^#(X(), x) -> c_6(proper^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ proper(c()) -> ok(c())
, match^#(X(), x) -> c_6(proper^#(x))
, proper^#(f(x)) -> c_8(f^#(proper(x)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, c_0() -> 5
, X_0() -> 9
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, f^#_0(3) -> 20
, f^#_0(5) -> 20
, f^#_0(9) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20
, match^#_0(3, 3) -> 23
, match^#_0(3, 5) -> 23
, match^#_0(3, 9) -> 23
, match^#_0(3, 11) -> 23
, match^#_0(3, 12) -> 23
, match^#_0(5, 3) -> 23
, match^#_0(5, 5) -> 23
, match^#_0(5, 9) -> 23
, match^#_0(5, 11) -> 23
, match^#_0(5, 12) -> 23
, match^#_0(9, 3) -> 23
, match^#_0(9, 5) -> 23
, match^#_0(9, 9) -> 23
, match^#_0(9, 11) -> 23
, match^#_0(9, 12) -> 23
, match^#_0(11, 3) -> 23
, match^#_0(11, 5) -> 23
, match^#_0(11, 9) -> 23
, match^#_0(11, 11) -> 23
, match^#_0(11, 12) -> 23
, match^#_0(12, 3) -> 23
, match^#_0(12, 5) -> 23
, match^#_0(12, 9) -> 23
, match^#_0(12, 11) -> 23
, match^#_0(12, 12) -> 23
, c_6_0(26) -> 23
, proper^#_0(3) -> 26
, proper^#_0(5) -> 26
, proper^#_0(9) -> 26
, proper^#_0(11) -> 26
, proper^#_0(12) -> 26}
11)
{active^#(f(x)) -> c_13(f^#(active(x)))}
The usable rules for this path are the following:
{ active(f(x)) -> mark(x)
, active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(x)
, active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))
, active^#(f(x)) -> c_13(f^#(active(x)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active(f(x)) -> mark(x)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(x)) -> mark(x)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(f(x)) -> c_13(f^#(active(x)))}
and weakly orienting the rules
{active(f(x)) -> mark(x)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(x)) -> c_13(f^#(active(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
found(x1) = [1] x1 + [0]
active^#(x1) = [1] x1 + [4]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(x)) -> f(active(x))
, f(ok(x)) -> ok(f(x))
, f(found(x)) -> found(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ active^#(f(x)) -> c_13(f^#(active(x)))
, active(f(x)) -> mark(x)}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, ok_0(3) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, found_0(3) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, active^#_0(3) -> 13
, active^#_0(11) -> 13
, active^#_0(12) -> 13
, f^#_0(3) -> 20
, f^#_0(11) -> 20
, f^#_0(12) -> 20}
12)
{ match^#(X(), x) -> c_6(proper^#(x))
, proper^#(c()) -> c_7()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
found(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(c()) -> c_7()}
Weak Rules: {match^#(X(), x) -> c_6(proper^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(c()) -> c_7()}
and weakly orienting the rules
{match^#(X(), x) -> c_6(proper^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(c()) -> c_7()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
found(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ proper^#(c()) -> c_7()
, match^#(X(), x) -> c_6(proper^#(x))}
Details:
The given problem does not contain any strict rules
13)
{match^#(X(), x) -> c_6(proper^#(x))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
found(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {match^#(X(), x) -> c_6(proper^#(x))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{match^#(X(), x) -> c_6(proper^#(x))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{match^#(X(), x) -> c_6(proper^#(x))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
found(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {match^#(X(), x) -> c_6(proper^#(x))}
Details:
The given problem does not contain any strict rules
14)
{active^#(f(x)) -> c_0()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
found(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(f(x)) -> c_0()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(x)) -> c_0()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(x)) -> c_0()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
c() = [0]
check(x1) = [0] x1 + [0]
start(x1) = [0] x1 + [0]
match(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
found(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0() = [0]
top^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
check^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
start^#(x1) = [0] x1 + [0]
match^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10() = [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(f(x)) -> c_0()}
Details:
The given problem does not contain any strict rules